(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const i0 Int)
(assert (= v6 v6 v3 v3 v1 v13 v11 v14 v16))
(assert v7)
(declare-const v17 Bool)
(assert (distinct v1 v6 v4 v7))
(push)
(declare-const v18 Bool)
(assert v6)
(declare-const v19 Bool)
(assert (= v3 v7))
(pop)
(declare-const v20 Bool)
(assert v7)
(assert (distinct (mod i0 81) i0))
(declare-const v24 Bool)
(push)
(assert (= i0 81))
(assert (not (not v8)))
(declare-const v25 Bool)
(assert (=> (not v0) (< (+ (div (mod i0 81) (- i0 81 (mod i0 81) (mod i0 81) i0)) (- i0 81 (mod i0 81) (mod i0 81) i0)) i0)))
(check-sat)
